$\forall$${\it the\_es}$:ES, $e$, ${\it e'}$:E.
\\[0ex](($e$ $<$loc ${\it e'}$) \& ($\forall$$e_{1}$:E. $\neg$(($e$ $<$loc $e_{1}$) \& ($e_{1}$ $<$loc ${\it e'}$)))) $\Rightarrow$ ($e$ = pred(${\it e'}$))